Library zayin_conjugate
Require Import PointsETC.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition zayin_conjugate P U :=
match P,U with
cTriple p q r, cTriple u v w ⇒
let h p q r x y z := p×(y + z)^2 - r×y^2 - q×z^2 + (p - r)*x×y + (p - q)*x×z in
cTriple (h p q r u v w) (h q r p v w u) (h r p q w u v)
end.
Lemma X2_is_zayin_conjugate_of_X1_X6 :
eq_points X_2 (zayin_conjugate X_1 X_6).
Proof.
intros.
red;simpl; repeat split; field; repeat split;try assumption.
Qed.
End Triangle.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition zayin_conjugate P U :=
match P,U with
cTriple p q r, cTriple u v w ⇒
let h p q r x y z := p×(y + z)^2 - r×y^2 - q×z^2 + (p - r)*x×y + (p - q)*x×z in
cTriple (h p q r u v w) (h q r p v w u) (h r p q w u v)
end.
Lemma X2_is_zayin_conjugate_of_X1_X6 :
eq_points X_2 (zayin_conjugate X_1 X_6).
Proof.
intros.
red;simpl; repeat split; field; repeat split;try assumption.
Qed.
End Triangle.